Weak omega-categories from intensional type theory

摘要

We show that for any type in Martin-L\"of Intensional Type Theory, the termsof that type and its higher identity types form a weak omega-category in thesense of Leinster. Precisely, we construct a contractible globular operad ofdefinable composition laws, and give an action of this operad on the terms ofany type and its identity types.